﻿/************************************************************************
 * SMLib - State Model Library
 * Copyright (C) 2012-2013 Ali Khalili (khalili_DOT_ir_@SIGN_gmail_DOT_com)
 * **********************************************************************
 * This program is free software; you can redistribute it and/or modify it
 * under the terms of the GNU Lesser General Public License (LGPL) published 
 * by the Free Software Foundation; either version 2.1 of the License, or (at your
 * option) any later version. This program is distributed without any
 * warranty. See the GNU Lesser General Public License for more details. 
 * ***********************************************************************
 * File         :     SMLib\Automata\MM\MealyUtils.cs
 * Description  :     Some utility function for Mealy machine
 * Change log   :     -Feb 2013:  Initial version
 * To Do        :     -implement functions!
 ************************************************************************/
using System;
using System.Collections.Generic;
using System.Text;
using SMLib.Automata.Base;
using SMLib.Automata.IA;
using SMLib.Base;
using SMLib.Utils;
using SMLib.DataTypes;

namespace SMLib.Automata.MM
{
    /// <summary>
    /// Some utility function for Mealy Machine.
    /// <remarks>[To Do: complete this class]</remarks>
    /// </summary>
    public class MealyUtils
    {
        /// <summary>
        /// Minimize/Reduce a Mealy machine: Construct a Canonical Form for a Mealy machine
        /// </summary>
        /// <remark>
        /// Partition refinement of states (order: node^2*|Sigma|)
        /// Based on Hopcroft [An nlogn algorithm for minimizing states in a finite automaton (1971)]
        /// <para>[To Do:] Implement based on (Marie-pierre Béal and Maxime Crochemore: "Minimizing incomplete automata", 2008)</para>
        /// </remark>
        /// <param name="m">the machine to be minimized</param>
        /// <returns>the computed minimise machine</returns>
        public static MealyMachine Minimize(MealyMachine m)
        {
            List<ValuedList<MealyMachine.Mealy_State, List<PairOfSymbols>>> allSets
                = new List<ValuedList<MealyMachine.Mealy_State, List<PairOfSymbols>>>();

            foreach (MealyMachine.Mealy_State n in m.GetStates())
            {
                ValuedList<MealyMachine.Mealy_State, List<PairOfSymbols>>
                    equivalents = new ValuedList<MealyMachine.Mealy_State, List<PairOfSymbols>>();
                equivalents.Add(n);
                allSets.Add(equivalents);
                equivalents.value = n.ListOfAllInputOutputs();
            }

            return null;
        }

        public static int CountEdge(MealyMachine m)
        {
            int counter = 0;
            foreach (MealyMachine.Mealy_State n in m.GetStates())
            {
                counter += n.Transitions.Count;
            }
            return counter;
        }

        public static int CountNondeterministicStates(MealyMachine m)
        {
            int counter = 0;
            foreach (MealyMachine.Mealy_State n in m.GetStates())
            {
                List<ISymbol> symbs = new List<ISymbol>();
                for (int i = 0; i < n.Transitions.Count; i++)
                {
                    if(symbs.Contains(n.Transitions[i].inLabel))
                    {
                        counter++;
                        break;
                    }
                    symbs.Add(n.Transitions[i].inLabel);
                }
            }
            return counter;
        }


        /// <summary>
        /// Conver a Mealy machine in C
        /// </summary>
        /// <param name="m"></param>
        /// <param name="path"></param>
        public static void SaveMealyinC(MealyMachine m, string path)
        {
            //int numberOfAlive;// = 1;
            //numberOfAlive = m.Size;
            StringBuilder cStringBulder = new StringBuilder();
			//* just to make sure they are correct!
			m.ComputeInputAlphabet();
			m.ComputeOutputAlphabet();
            
			string initCode = @"#define true  1
#define false 0

#include<WCHAR.H>
#include <string>
#include <iostream>
//************** EXPORT *************************
__declspec(dllexport) void __cdecl Reset();
//__declspec(dllexport) int  __cdecl Step(int input);
__declspec(dllexport) wchar_t *  __cdecl Step(wchar_t * inputStr);
//************** State ID ***********************
static int stateID = 0;
//************** input alphabet ******************
int InputSymbolToNumber(wchar_t * symbol){
//int result;
";
            int st = 0;

            foreach (ISymbol s in m.InputAlphabet.AllSymbols())
            {
                cStringBulder.Append("\tif(wcsicmp(symbol,L\"" + s.ToString() + "\")==0) return " + st + ";\n");
                st++;
            }
            cStringBulder.Append("\treturn -1;\n}");

            cStringBulder.Append("\n//********************************\n");

            cStringBulder.Append(
@"__declspec(dllexport) void __cdecl Reset(){
    stateID = 0;
}
");
            cStringBulder.Append("\n__declspec(dllexport) wchar_t *  __cdecl Step(wchar_t * inputStr){");
            cStringBulder.Append("\n\tint input=InputSymbolToNumber(inputStr);");
            st = 0;
            cStringBulder.Append("\r\n\tswitch (stateID){");
            foreach (MealyMachine.Mealy_State obj in m.GetStates())
            {
                cStringBulder.Append("\r\n\t\tcase " + st + ":");
                cStringBulder.Append("\r\n\t\t\tswitch (input){");
                foreach (MealyMachine.Mealy_Transition tr in obj.Transitions)
                {
                    int i = 0;
                    foreach (ISymbol s in m.InputAlphabet.AllSymbols())
                    {
                        if (tr.inLabel.Equals(s))
                        {
                            cStringBulder.Append("\r\n\t\t\t\tcase " + i + ":");
                            break;
                        }
                        else
                            i++;
                    }

                    int o = 0;
                    foreach (ISymbol s in m.OutputAlphabet.AllSymbols())
                    {
                        if (tr.outLabel.Equals(s))
                        {
                            int stID = 0;
                            foreach (MealyMachine.Mealy_State dest in m.GetStates())
                            {
                                if (dest == tr.Destination)
                                {
                                    cStringBulder.Append(" stateID = " + stID + ";");
                                    break;
                                }
                                else
                                    stID++;
                            }
                            cStringBulder.Append(" return /*" + o + "*/ L\"" + tr.outLabel + "\";");
                            break;
                        }
                        else
                            o++;
                    }
                }
                cStringBulder.Append("\r\n\t\t\t}\r\n\t\t\tbreak;");

                st++;
            }
            cStringBulder.Append("\r\n\t}\n}");
            System.IO.File.WriteAllText(path, initCode + cStringBulder.ToString());
        }


        const bool MakeMiddleStates = false;

        /// <summary>
        /// Translate a Mealy machine to an IA (to generate test cases for Mealy machines
        /// using the general IA test case generator). The IA would be exactly equal to the Mealy machine
        /// and all transitions would be Function Calls (to be as similar to Mealy as possible)
        /// <remarks>The approach is offline translation. The other approach could be an online translation</remarks>
        /// </summary>
        /// <param name="mealy">the input Mealt machine</param>
        /// <returns>the calculated IA</returns>
        public static InterfaceAutomaton ConvertToIOLTS(MealyMachine mealy)
        {
            InterfaceAutomaton myiolts = new InterfaceAutomaton();
            //* first, add all state into IA
            for (int i = 0; i < mealy.Size; i++)
            {
                InterfaceAutomaton.IA_State myState = new InterfaceAutomaton.IA_State(i);
                myiolts.AddState(myState);
            }

            //* then, process edges
            for (int i = 0; i < mealy.Size; i++)
            {
                //* Process State[i]
                for (int j = 0; j < mealy[i].Transitions.Count; j++)
                {
                    //* Process State[i].Transition[j]
                    int indexOfOther = -1;
                    for (int k = 0; k < mealy[i].Transitions.Count; k++)
                    {
                        if (k == j)
                            continue;

                        if (((mealy[i].Transitions[j]).inLabel).Equals(
                            ((mealy[i].Transitions[k]).inLabel)))
                        {
                            indexOfOther = k;
                            break;
                        }
                    }

                    if (indexOfOther == -1 || MakeMiddleStates == false)
                    {
                        //* Just one instance of this input: deterministic
                        InterfaceAutomaton.IA_Step myStep = new InterfaceAutomaton.IA_Step
                            ((mealy[i].Transitions[j]).Label);

                        for (int k = 0; k < mealy.Size; k++)
                        {
                            if (((mealy[i].Transitions[j]).Destination) == mealy[k])
                            {
                                myStep.SetDestination(myiolts[k]);
                                break;
                            }
                        }
                        (myiolts[i]).AddTransition(myStep);
                    }
                    else
                    {
                        //* More than one output for this input: non-deterministic
                        int indexOdDest = -1;
                        for (int k = 0; k < mealy.Size; k++)
                        {
                            if (((mealy[i].Transitions[j]).Destination) == mealy[k])
                            {
                                indexOdDest = k;
                                break;
                            }
                        }

                        if (indexOfOther < j)
                        {
                            //* the intermediate node was already constructed
                            foreach (InterfaceAutomaton.IA_Step s in (myiolts[i].Transitions))
                            {
                                if (s.Label.Equals((mealy[i].Transitions[j]).inLabel))
                                {
                                    //* the intermediate node found!
                                    InterfaceAutomaton.IA_State myIntermediateState = s.Destination;

                                    //* link from intermediate state into the real target
                                    InterfaceAutomaton.IA_Step myStep2 =
                                        new InterfaceAutomaton.IA_Step((mealy[i].Transitions[j]).outLabel, false);
                                    myStep2.SetDestination(myiolts[indexOdDest]);

                                    myIntermediateState.AddTransition(myStep2);
                                    break;
                                }
                            }
                        }
                        else
                        {
                            //* Create an intermediate step
                            InterfaceAutomaton.IA_State myIntermediateState = new InterfaceAutomaton.IA_State(myiolts.Size);
                            myiolts.AddState(myIntermediateState);

                            //* link to intermediate state
                            InterfaceAutomaton.IA_Step myStep1 =
                                new InterfaceAutomaton.IA_Step((mealy[i].Transitions[j]).inLabel, true);
                            myStep1.SetDestination(myIntermediateState);
                            (myiolts[i]).AddTransition(myStep1);

                            //* link from intermediate state into the real target
                            InterfaceAutomaton.IA_Step myStep2 =
                                new InterfaceAutomaton.IA_Step((mealy[i].Transitions[j]).outLabel, false);
                            myStep2.SetDestination(myiolts[indexOdDest]);
                            myIntermediateState.AddTransition(myStep2);
                        }
                    }
                }
            }
            return myiolts;
        }

        /// <summary>
        /// Make a Mealy machine "identifiable" using the power set construction
        /// </summary>
        /// <param name="m"></param>
        /// <returns></returns>
        public static MealyMachine Determinize(MealyMachine m)
        {
            //* create the machine
            MealyMachine dMachine = new MealyMachine();
            dMachine.InputAlphabet = m.InputAlphabet;
            dMachine.OutputAlphabet = m.OutputAlphabet;


            List<int> toBeExpanded = new List<int>();
            List<EnSet<MealyMachine.Mealy_State>> statesCont = new List<EnSet<MealyMachine.Mealy_State>>();
            EnSet<MealyMachine.Mealy_State> currStateCont = new EnSet<MealyMachine.Mealy_State>();
            statesCont.Add(currStateCont);

            //* create the first node into machine
            currStateCont.Add((MealyMachine.Mealy_State)m.InitialState);
            MealyMachine.Mealy_State m0 = new MealyMachine.Mealy_State("m0");
            dMachine.AddState(m0);

            //* add the first node in the processing list
            toBeExpanded.Add(0);
            int currentStateIndex;
            List<ISymbol> outs = new List<ISymbol>();

            //* star processing nodes not processed yet
            while (toBeExpanded.Count != 0)
            {
                //* remove the first node to be processed
                currStateCont = statesCont[toBeExpanded[0]];
                currentStateIndex = toBeExpanded[0];
                toBeExpanded.RemoveAt(0);

                //* create the next state
                EnSet<MealyMachine.Mealy_State> nextState;// = new SMLib.DataType.EnSet<MealyMachine.Mealy_State>();
                foreach (ISymbol i in m.InputAlphabet.AllSymbols())
                {
                    //* check all possible outputs
                    outs.Clear();
                    foreach (MealyMachine.Mealy_State st in currStateCont)
                    {
                        foreach (MealyMachine.Mealy_Transition tr in st.Transitions)
                        {
                            if (!tr.inLabel.Equals(i))
                                continue;

                            if (!outs.Contains(tr.outLabel))
                                outs.Add(tr.outLabel);
                        }
                    }
                    //* for each output, determine the next state
                    foreach (ISymbol o in outs)
                    {
                        nextState = new EnSet<MealyMachine.Mealy_State>();

                        foreach (MealyMachine.Mealy_State st in currStateCont)
                        {
                            foreach (MealyMachine.Mealy_Transition tr in st.Transitions)
                            {
                                if (!tr.outLabel.Equals(o) || !tr.inLabel.Equals(i))
                                    continue;

                                if (!nextState.Contains((MealyMachine.Mealy_State)tr.Destination))
                                    nextState.Add((MealyMachine.Mealy_State)tr.Destination);
                            }
                        }

                        //* check whether the next state exist or not
                        bool found = false;
                        int nextIndex = -1;
                        foreach (EnSet<MealyMachine.Mealy_State> st in statesCont)
                        {
                            nextIndex++;
                            if (st.Equals(nextState))
                            {
                                found = true;
                                break;
                            }
                        }

                        //* if not, add it to processing list
                        if (!found)
                        {
                            MealyMachine.Mealy_State m1 = new MealyMachine.Mealy_State("m" + (statesCont.Count).ToString());
                            dMachine.AddState(m1);

                            statesCont.Add(nextState);
                            toBeExpanded.Add(statesCont.Count - 1);
                            nextIndex = statesCont.Count - 1;
                        }
                        MealyMachine.Mealy_State src = ((MealyMachine.Mealy_State)dMachine.GetStates()[currentStateIndex]);
                        MealyMachine.Mealy_State dst = ((MealyMachine.Mealy_State)dMachine.GetStates()[nextIndex]);
                        src.AddTransition(dst, i, o);
                    }
                }


            }
            return dMachine;
        }

        /// <summary>
        /// Check that a mealy machine has "pure state nondeterminism" OR NEG (i.e. it is identifiable OR NEG)
        /// </summary>
        /// <param name="m"></param>
        /// <returns></returns>
        public bool isIdentifiable(MealyMachine m)
        {
            return false;
        }


        /// <summary>
        /// Trace an input word and generate the corresponding output
        /// <remarks>The important assumption is the the machine is DETERMINISTIC!</remarks>
        /// </summary>
        /// <param name="m">the machine</param>
        /// <param name="inputWord">the input word</param>
        /// <returns>the corresponding output word</returns>
        public static Word ExamineInputWord(MealyMachine m, Word inputWord)
        {
            Word o = new Word();
            MealyMachine.Mealy_State currentState = (MealyMachine.Mealy_State)m.InitialState;
            for (int i = 0; i < inputWord.Length; i++)
            {
                bool found = false;
                foreach (MealyMachine.Mealy_Transition t in currentState.Transitions)
                {
                    if (t.inLabel.Equals(inputWord[i]))
                    {
                        currentState = (MealyMachine.Mealy_State)t.Destination;
                        o.AddSymbol(t.outLabel);
                        found = true;
                        break;
                    }
                }
                if (!found)
                    throw new Exception("The trace doesn't exist!");
            }
            return o;
        }

        static Random rnd = new Random();


        /// <summary>
        /// Execute the machine one step
        /// </summary>
        /// <param name="currentNode">the current step</param>
        /// <param name="input">the stimuli</param>
        /// <param name="deterministic">whether the machine is deterministic or not</param>
        /// <returns>the response</returns>
        public static ISymbol Step(ref MealyMachine.Mealy_State currentNode, ISymbol input, bool deterministic = true)
        {
            if (deterministic)
            {
                foreach (MealyMachine.Mealy_Transition t in currentNode.Transitions)
                {
                    if (t.inLabel.Equals(input))
                    {
                        currentNode = (MealyMachine.Mealy_State)t.Destination;
                        return t.outLabel;
                    }
                }
                throw new Exception("The input is not in input alphabet!");
            }
            else
            {
                int numberOfOptions = 0;

                //* Count number of outputs
                foreach (MealyMachine.Mealy_Transition t in currentNode.Transitions)
                {
                    if (t.inLabel.Equals(input))
                    {
                        numberOfOptions++;
                    }
                }

                //* There is no onput corresponding this input!
                if (numberOfOptions < 1)
                {
                    throw new Exception("The input is not in input alphabet!");
                }
                // Return the only output
                else if (numberOfOptions == 1)
                {
                    foreach (MealyMachine.Mealy_Transition t in currentNode.Transitions)
                    {
                        if (t.inLabel.Equals(input))
                        {
                            currentNode = (MealyMachine.Mealy_State)t.Destination;
                            return t.outLabel;
                        }
                    }
                }
                // Select one random output among severals
                else
                {
                    int option = rnd.Next(numberOfOptions);
                    int counter = 0;
                    foreach (MealyMachine.Mealy_Transition t in currentNode.Transitions)
                    {
                        if (t.inLabel.Equals(input))
                        {
                            if (counter == option)
                            {
                                currentNode = (MealyMachine.Mealy_State)t.Destination;
                                return t.outLabel;
                            }
                            counter++;
                        }
                    }
                }
                // this never happens!
                return null;
            }
        }
    }
}
